<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>Postscript: 后记</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/lf.css" rel="stylesheet" type="text/css"/>

<body>

<div id="page">

<div id="header">
<a href='https://coq-zh.github.io/SF-zh/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 1: 逻辑基础</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>目录</li></a>
   <a href='coqindex.html'><li class='section_name'>索引</li></a>
   <a href='deps.html'><li class='section_name'>路线</li></a>
</ul>
</a></div>

<div id="main">

<h1 class="libtitle">Postscript<span class="subtitle">后记</span></h1>


<div class="doc">

<div class="paragraph"> </div>

 恭喜，课程终于顺利结束了！ 
<div class="paragraph"> </div>

<a name="lab398"></a><h1 class="section">回顾一下</h1>

<div class="paragraph"> </div>

 到目前为止，我们已经学习了很多内容。我们来快速地回顾一下：

<div class="paragraph"> </div>

<ul class="doclist">
<li> <b>函数式编程</b>：
<ul class="doclist">
<li> “声明式” 编程风格 (在不可变的数据构造上递归，而非在可变的数组或指针结构上循环）

</li>
<li> 高阶函数

</li>
<li> 多态 
</li>
</ul>

</li>
</ul>

<div class="paragraph"> </div>


<div class="paragraph"> </div>

<ul class="doclist">
<li> <b>逻辑</b>，软件工程的数学基础：
<pre>
           逻辑                微积分
        ---------   ~   ------------------
         软件工程          机械工程/土木工程
</pre>

<div class="paragraph"> </div>

<ul class="doclist">
<li> 归纳定义的集合和关系

</li>
<li> 归纳证明

</li>
<li> 证明对象 
</li>
</ul>

</li>
</ul>

<div class="paragraph"> </div>


<div class="paragraph"> </div>

<ul class="doclist">
<li> <b>Coq</b>，一个强有力的证明辅助工具
<ul class="doclist">
<li> 函数式核心语言

</li>
<li> 核心策略

</li>
<li> 自动化

</li>
</ul>

</li>
</ul>

</div>

<div class="doc">
<a name="lab399"></a><h1 class="section">继续前行</h1>

<div class="paragraph"> </div>

 假如本书的内容引起了你的兴趣，你还可以阅读<b>软件基础</b>系列的：

<div class="paragraph"> </div>

<ul class="doclist">
<li> <b>编程语言基础</b>（《软件基础》第二卷，与本书作者组类似）
             覆盖了了关于编程语言理论方面的研究生课程，包括霍尔逻辑
             （Hoare logic）、操作语义以及类型系统。

<div class="paragraph"> </div>


</li>
<li> <b>函数式算法验证</b>（《软件基础》第三卷，Andrew Appel 著）
             在使用 Coq 进行程序验证和函数式编程的基础之上，
             讨论了一般数据结构课程中的一系列主题并着眼于其形式化验证。
</li>
</ul>

</div>

<div class="doc">
<a name="lab400"></a><h1 class="section">其它资源</h1>

<div class="paragraph"> </div>

 进一步学习的资源……

<div class="paragraph"> </div>

<ul class="doclist">
<li> 本书包含了一些可选章节，其中讲述的内容或许会对你有用。你可以在
         <a href="toc.html">目录</a> 或
         <a href="deps.html">章节依赖简图</a> 中找到它们。

<div class="paragraph"> </div>


</li>
<li> 有关 Coq 的问题，可以查看 Stack Overflow 上的 <span class="inlinecode">#<span class="id" type="var">coq</span></span> 板块
         (<a href="https://stackoverflow.com/questions/tagged/coq"><span class="inlineref">https://stackoverflow.com/questions/tagged/coq</span></a>)，
         它是个很棒的社区资源。

<div class="paragraph"> </div>


</li>
<li> 更多与函数式编程相关的内容：
<ul class="doclist">
<li> Learn You a Haskell for Great Good, by Miran Lipovaca
              <a href="Bib.html#Lipovaca 2011"><span class="inlineref">[Lipovaca 2011]</span></a>.
              （《Haskell 趣学指南》<a href="https://learnyoua.haskell.sg/content/"><span class="inlineref">https://learnyoua.haskell.sg/content/</span></a>）

</li>
<li> Real World Haskell, by Bryan O'Sullivan, John Goerzen,
              and Don Stewart <a href="Bib.html#O'Sullivan 2008"><span class="inlineref">[O'Sullivan 2008]</span></a>.
              （《Real World Haskell 中文版》<a href="http://cnhaskell.com/"><span class="inlineref">http://cnhaskell.com/</span></a>）

</li>
<li> ……以及其它关于 Haskell、OCaml、 Scheme、Racket、Scala、F sharp
              等语言的优秀书籍。

<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> 更多 Coq 相关的资源：
<ul class="doclist">
<li> Certified Programming with Dependent Types, by Adam
             Chlipala <a href="Bib.html#Chlipala 2013"><span class="inlineref">[Chlipala 2013]</span></a>.

</li>
<li> Interactive Theorem Proving and Program Development:
             Coq'Art: The Calculus of Inductive Constructions, by Yves
             Bertot and Pierre Casteran <a href="Bib.html#Bertot 2004"><span class="inlineref">[Bertot 2004]</span></a>.

<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> 如果你有兴趣了解现实世界中形式化验证对关键软件的应用，
         可以参阅<b>《编程语言基础》</b>的后记。

<div class="paragraph"> </div>


</li>
<li> 关于使用 Coq 构建形式化验证的系统，可以参考 2017 年 DeepSpec
         夏令营的课程与相关资料。
         <a href="https://deepspec.org/event/dsss17/index.html"><span class="inlineref">https://deepspec.org/event/dsss17/index.html</span></a>

</li>
</ul>

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Oct&nbsp;28&nbsp;08:14:25&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>



</div>

</body>
</html>